public class Main {

	public static Node sample1() {

		Node Qx = new Node(Node.PREDICATE, "Q");
		Qx.addArg("x");
		Node PxNegated = new Node(Node.PREDICATE, "P");
		PxNegated.negate();
		PxNegated.addArg("x");
		Node implies = new Node(Node.IMPLIES);
		implies.left = Qx;
		implies.right = PxNegated;
		Qx.parent = implies;
		PxNegated.parent = implies;

		Node forAll = new Node(Node.FORALL);
		Node forAllVar = new Node(Node.VARIABLE, "x");
		forAll.left = forAllVar;
		forAll.right = implies;
		forAllVar.parent = forAll;
		implies.parent = forAll;

		Node Px = new Node(Node.PREDICATE, "P");
		Px.addArg("x");
		Node and = new Node(Node.AND);
		and.left = Px;
		and.right = forAll;
		Px.parent = and;
		forAll.parent = and;

		Node exist = new Node(Node.EXIST);
		Node existVar = new Node(Node.VARIABLE, "x");
		exist.left = existVar;
		exist.right = and;
		existVar.parent = exist;
		and.parent = exist;

		Node root = exist;
		root.parent = new Node(Node.DUMMY);
		root.parent.right = root;
		return root;
	}

	public static Node sample2() {
		Node Qy = new Node(Node.PREDICATE, "Q");
		Qy.addArg("y");
		Node Ryx = new Node(Node.PREDICATE, "R");
		Ryx.addArg("y");
		Ryx.addArg("x");

		Node and1 = new Node(Node.AND);
		and1.left = Qy;
		and1.right = Ryx;
		Qy.parent = and1;
		Ryx.parent = and1;

		Node exist = new Node(Node.EXIST);
		Node existVar = new Node(Node.VARIABLE, "y");
		exist.left = existVar;
		exist.right = and1;
		existVar.parent = exist;
		and1.parent = exist;

		Node Qx = new Node(Node.PREDICATE, "Q");
		Qx.addArg("x");
		Node and2 = new Node(Node.AND);
		and2.left = Qx;
		and2.right = exist;
		exist.parent = and2;
		Qx.parent = and2;

		Node Px = new Node(Node.PREDICATE, "P");
		Px.addArg("x");
		Node equal = new Node(Node.BICOND);
		equal.left = Px;
		equal.right = and2;
		Px.parent = equal;
		and2.parent = equal;

		Node forAll = new Node(Node.FORALL);
		Node forAllVar = new Node(Node.VARIABLE, "x");
		forAll.left = forAllVar;
		forAll.right = equal;
		forAllVar.parent = forAll;
		equal.parent = forAll;

		Node root = forAll;
		//root.parent = new Node(Node.DUMMY);
		//root.parent.right = root;
		return root;
	}

	public static void main(String[] args) {
		Node test = sample2();
		System.out.println(test);
		test.convertToCNF();
	}
}
